package sketch.specs.symbc;

import gov.nasa.jpf.symbc.SolvedPCResults;

import java.io.File;
import java.util.List;
import java.util.Map;

import org.eclipse.jdt.core.dom.CompilationUnit;

import sketch.ast.ASTUtils;
import sketch.jpf.symbc.SymbolicJPF;
import sketch.main.CodeToolkit;
import sketch.util.SketchUtil;
import junit.framework.Test;
import junit.framework.TestCase;
import junit.framework.TestSuite;

public class SymbolicExecDriverCreationTest extends TestCase {
	
	public static boolean run_symbc = false;
	
	public static Test suite() {
		return new TestSuite(SymbolicExecDriverCreationTest.class);
	}
	
	public void testCreateTesDriverAndCompileThem() {
		if(!run_symbc) {
			return;
		}
		
		CompilationUnit unit = ASTUtils.astRoot("./testfiles/sketch/specs/symbc/Mock_Unit_For_Testing.java");
		SymbolicExecDriverCreator creator = new SymbolicExecDriverCreator(unit);
		String[] extraImports = new String[] {"sketch.specs.symbc.auxiliary.Mock_Unit_For_Testing"};
		List<File> files = creator.createExecDriver(extraImports);
		CodeToolkit.compile(files);
		System.out.println("Compilation Successed!");
		
		//then run JPF on it
		for(File f : files) {
			String className = SketchUtil.transJavaFileNameToClassName(f.getName(), null);
			Class<?> clazz = CodeToolkit.loadClassFromDir(creator.getOutputDir(), className);
			System.out.println("Loadiing class: " + className);
			SymbolicJPF.execute(clazz, treemap.TreeMap.class, "remove");
			List<Map<String, Integer>> solvedIntValues = SolvedPCResults.solvedIntValues;
			String result = solvedIntValues.toString();
			System.out.println(result);
			SolvedPCResults.reset();
		}
	}
}
